0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 86 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 33 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 0 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
maxB_in_aag(s(T13), 0, s(T13)) → maxB_out_aag(s(T13), 0, s(T13))
maxB_in_aag(s(T23), s(T24), s(T23)) → U2_aag(T23, T24, lessA_in_ag(T24, T23))
lessA_in_ag(0, s(T31)) → lessA_out_ag(0, s(T31))
lessA_in_ag(s(T38), s(T37)) → U1_ag(T38, T37, lessA_in_ag(T38, T37))
U1_ag(T38, T37, lessA_out_ag(T38, T37)) → lessA_out_ag(s(T38), s(T37))
U2_aag(T23, T24, lessA_out_ag(T24, T23)) → maxB_out_aag(s(T23), s(T24), s(T23))
maxB_in_aag(T47, T46, T46) → U3_aag(T47, T46, lessA_in_ag(T47, s(T46)))
U3_aag(T47, T46, lessA_out_ag(T47, s(T46))) → maxB_out_aag(T47, T46, T46)
maxB_in_aag(0, T59, T59) → maxB_out_aag(0, T59, T59)
maxB_in_aag(s(T66), T65, T65) → U4_aag(T66, T65, lessA_in_ag(T66, T65))
U4_aag(T66, T65, lessA_out_ag(T66, T65)) → maxB_out_aag(s(T66), T65, T65)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
maxB_in_aag(s(T13), 0, s(T13)) → maxB_out_aag(s(T13), 0, s(T13))
maxB_in_aag(s(T23), s(T24), s(T23)) → U2_aag(T23, T24, lessA_in_ag(T24, T23))
lessA_in_ag(0, s(T31)) → lessA_out_ag(0, s(T31))
lessA_in_ag(s(T38), s(T37)) → U1_ag(T38, T37, lessA_in_ag(T38, T37))
U1_ag(T38, T37, lessA_out_ag(T38, T37)) → lessA_out_ag(s(T38), s(T37))
U2_aag(T23, T24, lessA_out_ag(T24, T23)) → maxB_out_aag(s(T23), s(T24), s(T23))
maxB_in_aag(T47, T46, T46) → U3_aag(T47, T46, lessA_in_ag(T47, s(T46)))
U3_aag(T47, T46, lessA_out_ag(T47, s(T46))) → maxB_out_aag(T47, T46, T46)
maxB_in_aag(0, T59, T59) → maxB_out_aag(0, T59, T59)
maxB_in_aag(s(T66), T65, T65) → U4_aag(T66, T65, lessA_in_ag(T66, T65))
U4_aag(T66, T65, lessA_out_ag(T66, T65)) → maxB_out_aag(s(T66), T65, T65)
MAXB_IN_AAG(s(T23), s(T24), s(T23)) → U2_AAG(T23, T24, lessA_in_ag(T24, T23))
MAXB_IN_AAG(s(T23), s(T24), s(T23)) → LESSA_IN_AG(T24, T23)
LESSA_IN_AG(s(T38), s(T37)) → U1_AG(T38, T37, lessA_in_ag(T38, T37))
LESSA_IN_AG(s(T38), s(T37)) → LESSA_IN_AG(T38, T37)
MAXB_IN_AAG(T47, T46, T46) → U3_AAG(T47, T46, lessA_in_ag(T47, s(T46)))
MAXB_IN_AAG(T47, T46, T46) → LESSA_IN_AG(T47, s(T46))
MAXB_IN_AAG(s(T66), T65, T65) → U4_AAG(T66, T65, lessA_in_ag(T66, T65))
MAXB_IN_AAG(s(T66), T65, T65) → LESSA_IN_AG(T66, T65)
maxB_in_aag(s(T13), 0, s(T13)) → maxB_out_aag(s(T13), 0, s(T13))
maxB_in_aag(s(T23), s(T24), s(T23)) → U2_aag(T23, T24, lessA_in_ag(T24, T23))
lessA_in_ag(0, s(T31)) → lessA_out_ag(0, s(T31))
lessA_in_ag(s(T38), s(T37)) → U1_ag(T38, T37, lessA_in_ag(T38, T37))
U1_ag(T38, T37, lessA_out_ag(T38, T37)) → lessA_out_ag(s(T38), s(T37))
U2_aag(T23, T24, lessA_out_ag(T24, T23)) → maxB_out_aag(s(T23), s(T24), s(T23))
maxB_in_aag(T47, T46, T46) → U3_aag(T47, T46, lessA_in_ag(T47, s(T46)))
U3_aag(T47, T46, lessA_out_ag(T47, s(T46))) → maxB_out_aag(T47, T46, T46)
maxB_in_aag(0, T59, T59) → maxB_out_aag(0, T59, T59)
maxB_in_aag(s(T66), T65, T65) → U4_aag(T66, T65, lessA_in_ag(T66, T65))
U4_aag(T66, T65, lessA_out_ag(T66, T65)) → maxB_out_aag(s(T66), T65, T65)
MAXB_IN_AAG(s(T23), s(T24), s(T23)) → U2_AAG(T23, T24, lessA_in_ag(T24, T23))
MAXB_IN_AAG(s(T23), s(T24), s(T23)) → LESSA_IN_AG(T24, T23)
LESSA_IN_AG(s(T38), s(T37)) → U1_AG(T38, T37, lessA_in_ag(T38, T37))
LESSA_IN_AG(s(T38), s(T37)) → LESSA_IN_AG(T38, T37)
MAXB_IN_AAG(T47, T46, T46) → U3_AAG(T47, T46, lessA_in_ag(T47, s(T46)))
MAXB_IN_AAG(T47, T46, T46) → LESSA_IN_AG(T47, s(T46))
MAXB_IN_AAG(s(T66), T65, T65) → U4_AAG(T66, T65, lessA_in_ag(T66, T65))
MAXB_IN_AAG(s(T66), T65, T65) → LESSA_IN_AG(T66, T65)
maxB_in_aag(s(T13), 0, s(T13)) → maxB_out_aag(s(T13), 0, s(T13))
maxB_in_aag(s(T23), s(T24), s(T23)) → U2_aag(T23, T24, lessA_in_ag(T24, T23))
lessA_in_ag(0, s(T31)) → lessA_out_ag(0, s(T31))
lessA_in_ag(s(T38), s(T37)) → U1_ag(T38, T37, lessA_in_ag(T38, T37))
U1_ag(T38, T37, lessA_out_ag(T38, T37)) → lessA_out_ag(s(T38), s(T37))
U2_aag(T23, T24, lessA_out_ag(T24, T23)) → maxB_out_aag(s(T23), s(T24), s(T23))
maxB_in_aag(T47, T46, T46) → U3_aag(T47, T46, lessA_in_ag(T47, s(T46)))
U3_aag(T47, T46, lessA_out_ag(T47, s(T46))) → maxB_out_aag(T47, T46, T46)
maxB_in_aag(0, T59, T59) → maxB_out_aag(0, T59, T59)
maxB_in_aag(s(T66), T65, T65) → U4_aag(T66, T65, lessA_in_ag(T66, T65))
U4_aag(T66, T65, lessA_out_ag(T66, T65)) → maxB_out_aag(s(T66), T65, T65)
LESSA_IN_AG(s(T38), s(T37)) → LESSA_IN_AG(T38, T37)
maxB_in_aag(s(T13), 0, s(T13)) → maxB_out_aag(s(T13), 0, s(T13))
maxB_in_aag(s(T23), s(T24), s(T23)) → U2_aag(T23, T24, lessA_in_ag(T24, T23))
lessA_in_ag(0, s(T31)) → lessA_out_ag(0, s(T31))
lessA_in_ag(s(T38), s(T37)) → U1_ag(T38, T37, lessA_in_ag(T38, T37))
U1_ag(T38, T37, lessA_out_ag(T38, T37)) → lessA_out_ag(s(T38), s(T37))
U2_aag(T23, T24, lessA_out_ag(T24, T23)) → maxB_out_aag(s(T23), s(T24), s(T23))
maxB_in_aag(T47, T46, T46) → U3_aag(T47, T46, lessA_in_ag(T47, s(T46)))
U3_aag(T47, T46, lessA_out_ag(T47, s(T46))) → maxB_out_aag(T47, T46, T46)
maxB_in_aag(0, T59, T59) → maxB_out_aag(0, T59, T59)
maxB_in_aag(s(T66), T65, T65) → U4_aag(T66, T65, lessA_in_ag(T66, T65))
U4_aag(T66, T65, lessA_out_ag(T66, T65)) → maxB_out_aag(s(T66), T65, T65)
LESSA_IN_AG(s(T38), s(T37)) → LESSA_IN_AG(T38, T37)
LESSA_IN_AG(s(T37)) → LESSA_IN_AG(T37)
From the DPs we obtained the following set of size-change graphs: